#include <vector>
#include <string>//???
#include <stdint.h>
#include <map>
#include <utility>
#include <sstream>
//debug
#include <sys/time.h>
//debug

#ifndef DIVINE_SYMBOLICS_H
#define DIVINE_SYMBOLICS_H

namespace divine {

const uint32_t bit_width = 32;//shouldn't be const, but for now...
const uint32_t distinct_inports = 0; //set to zero for full verification

//just two functions to ease reading and writing to blobs
template< typename Out >
void blobRead( Out *o, char **i ) {
  *o = *reinterpret_cast< Out* >( *i );
  *i += sizeof( Out );
}

template< typename In >
void blobWrite( char **o, In *i ) {
  *reinterpret_cast< In* >( *o ) = *i;
  *o += sizeof( In );
}

enum TYPE {VAR, INVAR, CON, OP};
  
enum OPTYPE {NOT, AND, OR, XOR, NAND, NOR, IMP,
             PLUS, TIMES, POW, SQRT, MIN, MAX,
             LT, LE, GT, GE, NEQ, EQ,
             CEIL, FLOOR, ROUND, FIX, //are we ready for floats?
             CAST, SWITCH, MSWITCH, BEET, ABS};

struct SMTRep;

struct Node {
  TYPE type;
  OPTYPE op;
  int arity;
  int name;
  int round;
  uint32_t value;
  std::vector< uint32_t > heirs;

  Node();
  Node( int );
  Node( const Node& );

  int size();
  void rebuild( char** );
  void store( char** );
};

struct Expr {
  std::vector< Node > nodes;
  uint32_t root; //never used, just for creating new expressions
  SMTRep *smt;

  Expr() {}
  Expr( SMTRep *);
  Expr( Expr & );
  Expr( const Expr & );
  Expr( Expr * );
  
  //special function for inport variables
  //new round requires new set of them
  void round( int );

  //substitute every variables named "order" with the expression *e
  void subs( int, Expr * );

  std::string convert( uint32_t, bool );
  std::string convert( std::string, bool );
  std::string translate( int, bool );
  std::string tran( uint32_t, bool, int );
  std::string print();
  
  void clear();
  int size();
  void rebuild( char** );
  void store( char** );
};

struct SMTRep
{
  //the original system
  struct OrSys {
    std::vector< Expr > delays_expr;
    std::vector< std::string > delays_name;
    std::vector< Expr > outports_expr;
    std::vector< std::string > outports_name;
    std::vector< std::pair< uint32_t, uint32_t > > inports_range;
    std::vector< std::string > inports_name;

    OrSys( const OrSys &o ) {
      delays_expr = o.delays_expr;
      delays_name = o.delays_name;
      outports_expr = o.outports_expr;
      outports_name = o.outports_name;
      inports_range = o.inports_range;
      inports_name = o.inports_name;
    }

    OrSys() {}
  };

  OrSys os;
  //the current round of inport variables
  int round;

  std::vector< uint32_t > in_values; //for counterexample
  //state is represented by pc and delay expressions
  std::vector< Expr > curDelays;
  std::vector< Expr > pc;
  std::vector< Expr > lastPC;

  bool cond_tick;
  int offset;

  //debug stuff
  timeval timer;
  int counter;

  void startTimer() { gettimeofday( &timer, NULL ); }
  uint32_t endTimer() {
    timeval tmp;
		gettimeofday( &tmp, NULL );
		tmp.tv_sec -= timer.tv_sec;
		tmp.tv_usec -= timer.tv_usec;
		if ( tmp.tv_usec < 0 ) {
				tmp.tv_usec += 1000000;
				tmp.tv_sec--;
		}
		return uint32_t( (tmp.tv_usec + tmp.tv_sec * 1000000) / 1000 );
  }

  struct Report {
    uint32_t checks;
    uint32_t time;
    uint32_t size;
    uint32_t state_size;
    uint32_t assertions;
  };
  
  std::vector< Report > times;
  //debug stuff

  SMTRep();
  SMTRep( SMTRep * );
  
  void tick();
  int size();
  
  std::string convert( uint32_t, bool );
  void read( char* );
  void write( char* );
  std::string print();
  void verify_consistency();
  void initialise();
  int by_name( std::string );

  bool pc_sat( bool );
  void addToPath( Expr * );
  void translate( std::vector< Expr > *, char * );
  int get_round( std::vector< Expr > * );

  //check if these expressions are identical
  bool check_ide( std::vector< Expr > *, std::vector< Expr > *,
                  std::vector< Expr > *, std::vector< Expr > * );
  
  //external functions to be called from hashset
  int find( std::vector< std::vector< Expr > > *,
            std::vector< std::vector< Expr > > *, char * );
  int addIfNew( std::vector< std::vector< Expr > > *,
                std::vector< std::vector< Expr > > *, char * );
  void add( std::vector< std::vector< Expr > > *,
            std::vector< std::vector< Expr > > *, char * );
};

}
#endif
